p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))).
(n:, i:{0..n}. f(i) < f(n))
 (n:. 0  X(n))
 (m:, n:{0..(m+1)}. rv-partial-sum(n;i.X(i))  rv-partial-sum(m;i.X(i))) 

latex

Definitions

x:A. B(x), , x(s), P  Q, t  T, , i  j , A  B, A, False, {i..j}, X  Y, rv-partial-sum(n;i.X(i)), SQType(T), {T}, x. t(x), i  j < k, P & Q, , Top, rv-const(a), X + Y, S  T, suptype(S; T), P  Q, a  b, P  Q, T, True, Dec(P), P  Q, RandomVariable(p;n), Outcome

Lemmas

rv-le wf, rv-const wf, int inc rationals, int seg wf, le wf, nat wf, random-variable wf, finite-prob-space wf, decidable int equal, nat properties, ge wf, p-outcome wf, qsum wf, rationals wf, subtype rel function, qle weakening eq qorder, rv-partial-sum-unroll, rv-partial-sum wf, qle wf, qadd wf, qle functionality wrt implies, iff transitivity, qmul wf, qadd preserves qle, squash wf, true wf, qadd comm q, qadd ac 1 q, qinverse q, qadd inv assoc q